The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), y, ys, x, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, y, ys, x, xs) → False
eqNatList[Ite](True, y, ys, x, xs) → eqNatList(xs, ys)

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
prefix(Cons(x', xs'), Cons(x, xs)) →⁺ and(!EQ(x', x), prefix(xs', xs))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [xs' / Cons(x', xs'), xs / Cons(x, xs)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), y, ys, x, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, y, ys, x, xs) → False
eqNatList[Ite](True, y, ys, x, xs) → eqNatList(xs, ys)

Rewrite Strategy: INNERMOST

(5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
eqNatList[Ite]/1
eqNatList[Ite]/3

(6) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) → False
eqNatList[Ite](True, ys, xs) → eqNatList(xs, ys)

Rewrite Strategy: INNERMOST

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

Innermost TRS:
Rules:
prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) → False
eqNatList[Ite](True, ys, xs) → eqNatList(xs, ys)

Types:
prefix :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
Cons :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
and :: False:True → False:True → False:True
!EQ :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
domatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
Nil :: Cons:Nil:S:0'
False :: False:True
True :: False:True
domatch[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
eqNatList :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
eqNatList[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
notEmpty :: Cons:Nil:S:0' → False:True
strmatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
S :: Cons:Nil:S:0' → Cons:Nil:S:0'
0' :: Cons:Nil:S:0'
hole_False:True1_0 :: False:True
hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0'
gen_Cons:Nil:S:0'3_0 :: Nat → Cons:Nil:S:0'

(9) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
prefix, !EQ, domatch, eqNatList

They will be analysed ascendingly in the following order:
!EQ < prefix
prefix < domatch
!EQ < eqNatList

(10) Obligation:

Innermost TRS:
Rules:
prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) → False
eqNatList[Ite](True, ys, xs) → eqNatList(xs, ys)

Types:
prefix :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
Cons :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
and :: False:True → False:True → False:True
!EQ :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
domatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
Nil :: Cons:Nil:S:0'
False :: False:True
True :: False:True
domatch[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
eqNatList :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
eqNatList[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
notEmpty :: Cons:Nil:S:0' → False:True
strmatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
S :: Cons:Nil:S:0' → Cons:Nil:S:0'
0' :: Cons:Nil:S:0'
hole_False:True1_0 :: False:True
hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0'
gen_Cons:Nil:S:0'3_0 :: Nat → Cons:Nil:S:0'

Generator Equations:
gen_Cons:Nil:S:0'3_0(0) ⇔ Nil
gen_Cons:Nil:S:0'3_0(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil:S:0'3_0(x))

The following defined symbols remain to be analysed:
!EQ, prefix, domatch, eqNatList

They will be analysed ascendingly in the following order:
!EQ < prefix
prefix < domatch
!EQ < eqNatList

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol !EQ.

(12) Obligation:

Innermost TRS:
Rules:
prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) → False
eqNatList[Ite](True, ys, xs) → eqNatList(xs, ys)

Types:
prefix :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
Cons :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
and :: False:True → False:True → False:True
!EQ :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
domatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
Nil :: Cons:Nil:S:0'
False :: False:True
True :: False:True
domatch[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
eqNatList :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
eqNatList[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
notEmpty :: Cons:Nil:S:0' → False:True
strmatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
S :: Cons:Nil:S:0' → Cons:Nil:S:0'
0' :: Cons:Nil:S:0'
hole_False:True1_0 :: False:True
hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0'
gen_Cons:Nil:S:0'3_0 :: Nat → Cons:Nil:S:0'

Generator Equations:
gen_Cons:Nil:S:0'3_0(0) ⇔ Nil
gen_Cons:Nil:S:0'3_0(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil:S:0'3_0(x))

The following defined symbols remain to be analysed:
prefix, domatch, eqNatList

They will be analysed ascendingly in the following order:
prefix < domatch

(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
prefix(gen_Cons:Nil:S:0'3_0(+(1, n28_0)), gen_Cons:Nil:S:0'3_0(+(1, n28_0))) → *4_0, rt ∈ Ω(n28₀)

Induction Base:
prefix(gen_Cons:Nil:S:0'3_0(+(1, 0)), gen_Cons:Nil:S:0'3_0(+(1, 0)))

Induction Step:
prefix(gen_Cons:Nil:S:0'3_0(+(1, +(n28_0, 1))), gen_Cons:Nil:S:0'3_0(+(1, +(n28_0, 1)))) →_R^Ω(1)
and(!EQ(Nil, Nil), prefix(gen_Cons:Nil:S:0'3_0(+(1, n28_0)), gen_Cons:Nil:S:0'3_0(+(1, n28_0)))) →_IH
and(!EQ(Nil, Nil), *4_0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(14) Complex Obligation (BEST)

(15) Obligation:

Innermost TRS:
Rules:
prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) → False
eqNatList[Ite](True, ys, xs) → eqNatList(xs, ys)

Types:
prefix :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
Cons :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
and :: False:True → False:True → False:True
!EQ :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
domatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
Nil :: Cons:Nil:S:0'
False :: False:True
True :: False:True
domatch[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
eqNatList :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
eqNatList[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
notEmpty :: Cons:Nil:S:0' → False:True
strmatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
S :: Cons:Nil:S:0' → Cons:Nil:S:0'
0' :: Cons:Nil:S:0'
hole_False:True1_0 :: False:True
hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0'
gen_Cons:Nil:S:0'3_0 :: Nat → Cons:Nil:S:0'

Lemmas:
prefix(gen_Cons:Nil:S:0'3_0(+(1, n28_0)), gen_Cons:Nil:S:0'3_0(+(1, n28_0))) → *4_0, rt ∈ Ω(n28₀)

Generator Equations:
gen_Cons:Nil:S:0'3_0(0) ⇔ Nil
gen_Cons:Nil:S:0'3_0(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil:S:0'3_0(x))

The following defined symbols remain to be analysed:
domatch, eqNatList

(16) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol domatch.

(17) Obligation:

Innermost TRS:
Rules:
prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) → False
eqNatList[Ite](True, ys, xs) → eqNatList(xs, ys)

Types:
prefix :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
Cons :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
and :: False:True → False:True → False:True
!EQ :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
domatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
Nil :: Cons:Nil:S:0'
False :: False:True
True :: False:True
domatch[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
eqNatList :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
eqNatList[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
notEmpty :: Cons:Nil:S:0' → False:True
strmatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
S :: Cons:Nil:S:0' → Cons:Nil:S:0'
0' :: Cons:Nil:S:0'
hole_False:True1_0 :: False:True
hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0'
gen_Cons:Nil:S:0'3_0 :: Nat → Cons:Nil:S:0'

Lemmas:
prefix(gen_Cons:Nil:S:0'3_0(+(1, n28_0)), gen_Cons:Nil:S:0'3_0(+(1, n28_0))) → *4_0, rt ∈ Ω(n28₀)

Generator Equations:
gen_Cons:Nil:S:0'3_0(0) ⇔ Nil
gen_Cons:Nil:S:0'3_0(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil:S:0'3_0(x))

The following defined symbols remain to be analysed:
eqNatList

(18) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol eqNatList.

(19) Obligation:

Innermost TRS:
Rules:
prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) → False
eqNatList[Ite](True, ys, xs) → eqNatList(xs, ys)

Types:
prefix :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
Cons :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
and :: False:True → False:True → False:True
!EQ :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
domatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
Nil :: Cons:Nil:S:0'
False :: False:True
True :: False:True
domatch[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
eqNatList :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
eqNatList[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
notEmpty :: Cons:Nil:S:0' → False:True
strmatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
S :: Cons:Nil:S:0' → Cons:Nil:S:0'
0' :: Cons:Nil:S:0'
hole_False:True1_0 :: False:True
hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0'
gen_Cons:Nil:S:0'3_0 :: Nat → Cons:Nil:S:0'

Lemmas:
prefix(gen_Cons:Nil:S:0'3_0(+(1, n28_0)), gen_Cons:Nil:S:0'3_0(+(1, n28_0))) → *4_0, rt ∈ Ω(n28₀)

Generator Equations:
gen_Cons:Nil:S:0'3_0(0) ⇔ Nil
gen_Cons:Nil:S:0'3_0(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil:S:0'3_0(x))

No more defined symbols left to analyse.

(20) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
prefix(gen_Cons:Nil:S:0'3_0(+(1, n28_0)), gen_Cons:Nil:S:0'3_0(+(1, n28_0))) → *4_0, rt ∈ Ω(n28₀)

(21) BOUNDS(n^1, INF)

(22) Obligation:

Innermost TRS:
Rules:
prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) → False
eqNatList[Ite](True, ys, xs) → eqNatList(xs, ys)

Types:
prefix :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
Cons :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
and :: False:True → False:True → False:True
!EQ :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
domatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
Nil :: Cons:Nil:S:0'
False :: False:True
True :: False:True
domatch[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
eqNatList :: Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
eqNatList[Ite] :: False:True → Cons:Nil:S:0' → Cons:Nil:S:0' → False:True
notEmpty :: Cons:Nil:S:0' → False:True
strmatch :: Cons:Nil:S:0' → Cons:Nil:S:0' → Cons:Nil:S:0'
S :: Cons:Nil:S:0' → Cons:Nil:S:0'
0' :: Cons:Nil:S:0'
hole_False:True1_0 :: False:True
hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0'
gen_Cons:Nil:S:0'3_0 :: Nat → Cons:Nil:S:0'

Lemmas:
prefix(gen_Cons:Nil:S:0'3_0(+(1, n28_0)), gen_Cons:Nil:S:0'3_0(+(1, n28_0))) → *4_0, rt ∈ Ω(n28₀)

Generator Equations:
gen_Cons:Nil:S:0'3_0(0) ⇔ Nil
gen_Cons:Nil:S:0'3_0(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil:S:0'3_0(x))

No more defined symbols left to analyse.

(23) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
prefix(gen_Cons:Nil:S:0'3_0(+(1, n28_0)), gen_Cons:Nil:S:0'3_0(+(1, n28_0))) → *4_0, rt ∈ Ω(n28₀)

(24) BOUNDS(n^1, INF)